Step of Proof: gen_hyp_tp 9,38
Inference at * 1 1 4 2 1 3 
Iof proof for Lemma gen hyp tp:

.....equality..... NILNIL

1. A : Type
2. e : A
3. H : AType
4. x : A
5. e = x
6. H(e)
7. A  Type
8. e  A
9. x:A. (e = x)  Type
  e = x 
latex
 by %L:equality% 
Id 
latex

Id1: .....equality..... NILNIL

Id1:   e = x
Id.

origin